\documentclass{article}
\usepackage{xcolor} 
\usepackage{fullpage} 
\usepackage{amsmath}
\usepackage{amssymb}
\usepackage{proof}
\usepackage{hyperref}
\usepackage{caption}
\usepackage{comment}
\usepackage{subcaption}
\usepackage{fancybox}
\usepackage{stmaryrd}
\definecolor{light-gray}{gray}{0.86}
\newcommand{\nil}[0]{\mathsf{nil}} 
\newcommand{\cons}[0]{\mathsf{cons}} 
\newcommand{\vecc}[0]{\mathsf{vec}} 
\newcommand{\suc}[0]{\mathsf{S}} 
\newcommand{\nat}[0]{\mathsf{Nat}} 
\newcommand{\ind}[0]{\mathsf{Ind}} 
\newcommand{\app}[0]{\mathsf{app}} 
\newcommand{\selfstar}[0]{$\mathsf{Selfstar}\ $} 
\newcommand{\self}[0]{\mathbf{S}} 
\newcommand{\fomega}[0]{\mathbf{F}_{\omega}} 
\newcommand{\cc}[0]{\mathbf{CC}} 
\newcommand{\gray}[1]{\colorbox{light-gray}{#1}}
\newcommand{\mgray}[1]{\colorbox{light-gray}{$#1$}}
\newcommand{\M}[3]{
\{#1_i \mapsto #2_i\}_{i \in #3}} 
\newcommand{\Mb}[4]{
\{#1_i:#4_i \mapsto #2_i\}_{i \in #3}} 
\newcommand{\interp}[1]{\llbracket #1 \rrbracket} 
\newcommand{\mylet}[2]{\mathbf{let}\ #1 \ \mathbf{in} \ #2} 
\newcommand{\mycase}[2]{\mathbf{case}\ #1 \ \mathbf{of} \ \{ #2 \}_{i\in {N}}} 
\newcommand{\bm}[4]{
\{(#1_i:#2_i) \mapsto #3_i\}_{i \in #4}} 
\newcommand{\frank}[1]{\textcolor{blue}{\textbf{[#1 ---Frank]}}}
%% \newarrowfiller{dasheq} {==}{==}{==}{==}
%% \newarrow {Mapsto} |--->
%% \newarrow {Line} -----
%% \newarrow {Implies} ===={=>}
%% \newarrow {EImplies} {}{dasheq}{}{dasheq}{=>}
%% \newarrow {Onto} ----{>>}
%% \newarrow {DashInto} C{dash}{}{dash}{>}
%% \newarrow {Dashto}{}{dash}{}{dash}{>}
%% \newarrow {Dashtoo}{}{dash}{}{dash}{>>}

\newtheorem{lemma}{Lemma}
\newtheorem{definition}{Definition}
\newtheorem{example}{Example}
\newtheorem{procedure}{Procedure}
% for page numbers:
\pagestyle{plain}

\begin{document}
\title{A Logic Programming Approach for Type Class Inference}

\author{Peng Fu}
\date{\today}


\maketitle

\begin{abstract}
1. Some examples of that current Haskell type checker
can't handle elegantly, including but not limited to: Tom's example, and the infinite growing
example.a 

2. Connecting the use of LP to type class inference in the style of SPJ's design choice paper. 

3. Formalized a version of CoALP suited for Haskell's type class inference.  

4. Formalized and implement a working prototype. 
\end{abstract}

\section{Specification} 
\begin{definition}[Syntax]

\

\noindent \textit{Expression} $t \ :: = \ x \ | \ \lambda x.t \ | \ t\ t' \ | \ \mathbf{let}\ x = t\ \mathbf{in}\ t' \ | \ \mathbf{case} \ t \ \mathbf{of}\ \{ p_i \to t_i \}_{i \in {N}} $

\noindent \textit{Pattern} $p \ ::= x \ | \ p\ x$

\noindent \textit{Monomorphic Types} $T \ ::= B \ | \ X \ | \ T_1 \to T_2 \ | \ T \ T'$

\noindent \textit{Type Class} $U \ ::= X \ T \ | \ U \ T$

\noindent \textit{Qualifiers} $P ::= \ \cdot \ | \ P, U$

\noindent \textit{Qualified Types} $Q \ ::=  P \Rightarrow T$

\noindent \textit{Polymorphic Types} $S \ ::= \ Q \ | \ \forall X. S$

\noindent \textit{Kinds} $\kappa \ ::= \ * \ | \ \kappa' \to \kappa$ 

\noindent \textit{Context} $\Gamma \ :: = \ \cdot \ | \ \Gamma, x:S$ 

%% \noindent \textit{Definitions} $\mu \ ::= \ \bm{x}{S^{\kappa}}{t}{N}\cup \M{X^{\kappa}} {T^{\kappa}}{M}$

%% \noindent \textit{Term definitions} $\rho \ ::= \ \M{x}{t}{N}$
  
\end{definition}

Note that data type constructors is a subset of term variables. Patterns is a subset of expression. $B$ is a meta-variable stands for constant types. Note that here we only work with simple pattern, since there is a procedure to translate nested pattern into simple pattern. 
\begin{definition}[Declarations]
  \
  
\noindent Term declaration: $\Delta\ ::= \cdot \ | \ \Delta, x = t$
 
\noindent Class declaration:  $C \ ::=\ \cdot\ | \ C, \mathbf{class} \ U \ \mathbf{where}\ \Gamma$

\noindent Instance declaration:  $I \ ::=\ \cdot\ | \ I, \mathbf{instance} \ P \Rightarrow \ U\ \mathbf{where}\ \Delta$

\noindent Data declaration:  $E \ ::=\ \cdot\ | \ E, \mathbf{data} \ D \ \mathbf{where}\ \Gamma$

\noindent Data head $D \ ::= \ X \ | \ D \ X$

\
\end{definition}

We assume a preprocess that brings multiple equations for function definitions into a single 
lambda term with case expression and annotates the type of a method with corresponding type class qualifier. 

Note that in this article, we are not going to deal with \textit{subtyping}, namely, class declaration of the form $\mathbf{class} \ U_1,..., U_n \Rightarrow U \ \mathbf{where}\ \Gamma$, where $U_1,..., U_n$ are \textit{superclass} of $U$. I think it will cause a confusion/illusion of 
OO, e.g., consider $\mathbf{class} \ \mathrm{Eq}\ A \Rightarrow \mathrm{Ord} \ A $, potentially
we could have $\mathrm{eq} : \mathrm{Eq}\ A \to (A \to A \to \mathsf{Bool})$ and $\mathrm{eq} : \mathrm{Ord}\ A \to (A \to A \to \mathsf{Bool})$, but what we really means is something likes $\mathrm{eq}_1 : \mathrm{Eq}\ A \to (A \to A \to \mathsf{Bool})$ and $\mathrm{eq}_2 : \mathrm{Ord}\ A \to (A \to A \to \mathsf{Bool})$, unless we decided to use type information as well as identifier to identify entity, we are not going to support subtyping\footnote{A discussion about why Haskell's type class is not subtyping can be found at \url{https://news.ycombinator.com/item?id=4784116}}.  

Note that for the type annotation in the data type declaration, we are not
allowing the type to contains any type class quanlifiers\footnote{Why? ``The designers of Haskell 98 do now think, that it was a bad decision to allow constraints on constructors.'' \url{http://www.haskell.org/haskellwiki/Data_declaration_with_constraint}}. Another reason for this restriction is that one typically need to lift this restriction in order to handle GADT, thus the notion of type class could be use to handle equality between types, for example, say we have a type class definition $\mathbf{class} \ \mathrm{TEq}\ a\ b\ \mathbf{where}...$ to express type $a$ and type $b$ are equal, but what would be the default method and its type here? I have no idea 
what the method would be, thus making it impossible to construct runtime evidence. Or, one may think to do something likes $\forall C. C\ a \Rightarrow C\ b $, but then we are now quantifying
over type class, which is going beyond the expressiveness of traditional logic programs. In this article, we enforce this restriction only for the sake of simplicity. 


\begin{definition}[Declarative Typing] \fbox{$P, \Gamma \vdash t : S$}

  \
  
  \begin{tabular}{lll}
  \infer{P , \Gamma \vdash x : S }    
        {(x : S) \in \Gamma}
        &
        &
   \infer{P , \Gamma \vdash t\ t' : T}    
        {P , \Gamma \vdash t : T' \to T & P, \Gamma \vdash t' : T'}
        \\
        \\
    \infer{P, \Gamma \vdash \lambda x. t : T \to T'}    
          {P, \Gamma, x: T \vdash t: T'}
     &
          &
          \infer{P_1 , P_2, \Gamma \vdash \mylet{x = t}{t'} : T }{P_1, \Gamma \vdash t : S & P_2, \Gamma, x : S \vdash t' : T}
          \\
          \\
          \infer{P, \Gamma \vdash t : [T/X]S}{P, \Gamma \vdash t : \forall X. S}
          
          & &
          \infer{P, \Gamma \vdash t : \forall X. S}{P, \Gamma \vdash t : S & X \notin \mathrm{FV}(\Gamma) \cup \mathrm{FV}(P)}
          \\
          \\
          \infer{P, \Gamma \vdash t : P', P'' \Rightarrow T}{P, P', \Gamma \vdash t : P'' \Rightarrow T }
          & &
          \infer{P, \Gamma \vdash t : P'' \Rightarrow T}{ P, \Gamma \vdash t : P', P'' \Rightarrow T & \Phi \vdash P' }
          
          \\
          \\
          \infer{P, \Gamma \vdash \mycase{t}{p_i \to t_i} : T}{P, \Gamma \vdash t : [\underline{{T}}/\underline{X}]D & \{P, \Gamma, \Gamma_{p_i} \vdash t_i: T\}_{i\in N}}
  \end{tabular}
  
\end{definition}

Note that $\Gamma_{p_i}$ means a context constructed from simple pattern $p_i$ according
to the data declaration of $D$. For example, if $p_i \equiv c \ x_1... x_n$, and $c :\forall \underline{X}.  T_1 \to ... \to T_n \to D$,
then $\Gamma_{p_i} \equiv \{x_1: [\underline{T}/\underline{X}]T_1,..., x_n : [\underline{T}/\underline{X}]T_n\} $. 

$\Phi \vdash P' $ is intended to mean the query of $P'$ is successful with regard to the logic programs induced by the instance delaration $I$. 

\begin{definition}[Logic Program]
Let $I$ be the instance delarations of the form $\{\mathbf{instance}\ P_i \Rightarrow U_i\ \mathbf{where}\ \Delta_i \}_{i\in N}$. We say $\Phi = \{P_i \Rightarrow U_i\}_{i \in N}$ is the logic program induced by $I$. \footnote{Note that we could represent $\Phi$ as $\{U_i \Leftarrow P_i\}_{i \in N}$, which would be closer to the traditional treatment of logic program. } 
\end{definition}

\begin{definition}[Cut Rule]
\
The inference engine for our logic programs is the following:

\
  
  \infer[cut]{P,P' \Rightarrow U}{P \Rightarrow U_1 & P', U_1 \Rightarrow U}
\end{definition}

Note that the word \textit{cut} here is not related to the ``cut operator'' in Prolog.

\begin{definition}[Logical Query]
 We write $\Phi \vdash U$ to mean $ \Rightarrow U$ is derivable from $\Phi$ using the cut rule.
We write $\Phi \vdash P$ to mean $ \Rightarrow U$($U$ is a fresh type variable) is derivable from $\Phi \cup \{P \Rightarrow U\}$ using the cut rule.
\end{definition}

Some $\mathrm{Eq}\ A$ examples. 
\section{Algorithmic Specification}
\begin{definition}
  \fbox{$W(\Gamma, t) = (t', S, \Sigma, \sigma)$}

  \
  
  \begin{itemize}
  \item $W(\Gamma, x) = (x \ e,  [Y/X]T, [e : [Y/X]U], \emptyset )$, where
        $(x : \forall X. U \Rightarrow T) \in \Gamma$, $Y$ is a new type variable, $e$ is a 
    new term variable. % and $\Psi \vdash [Y/X]U$. 
        
    \item $W(\Gamma, t\ t') = ( t_1\ t_2, \sigma Y, \sigma [\sigma_2\Sigma,\Sigma'] ,\sigma \cdot \sigma_2 \cdot \sigma_1)$, where $W(\Gamma, t) = (t_1, T, \Sigma, \sigma_1)$, 
      $W(\sigma_1 \Gamma, t') = (t_2, T', \Sigma', \sigma_2)$, $Y$ is a new type variable and
      $\sigma = \mathrm{mgu}(\sigma_2 T, T' \to Y)$.
    
\item $W(\Gamma, \lambda x. t) = (\lambda x.t', \sigma Y \to T, \Sigma, \sigma)$, where $W((\Gamma, x:Y), t) = (t', T, \Sigma, \sigma)$
  and $Y$ is a new type variable.

  \item $W(\Gamma, \mylet{x = t}{t'}) = (\mylet{x = t_1}{t_2}, T', \Sigma', \sigma_2 \cdot \sigma_1) $ where $W(\Gamma, t) = (t_1, T, \Sigma_1, \sigma_1)$,
    $S = \mathrm{gen}(\sigma_1 \Gamma, P_{\Sigma_1} \Rightarrow T)$, $W((\sigma_1 \Gamma, x : S), t') = (t_2, T', \Sigma', \sigma_2)$. 

    \item $ W(\Gamma,\mycase{t}{p_i \to t_i}) = (\mycase{t'}{p_i \to t_i'}, \sigma_n T_n, \sigma_n[\Sigma_0,..., \Sigma_n], \sigma_n)$, where $W(\Gamma, t) = (t', T_1, \Sigma_1, \sigma_1)$; $W((\Gamma, \Gamma_{p_0}), t_0) = (t_0', T_0, \Sigma_0, \sigma_0)$; for $i = 1,...,n$, 
      $W(\sigma_{i-1}(\Gamma, \Gamma_{p_i}), t_i) = (t_i', T_i, \Sigma_i, \sigma_i')$, $\sigma_i = \mathrm{mgu}(\sigma_i' T_{i-1}, T_i) \cdot \sigma_i'$. 
  \end{itemize}
  

\end{definition}

Note that in the inference algorithm, we delay the checking of $\Sigma$, so in practice, 
we may want to check the validity of $\Sigma$ \textit{at the call site}. We could just not perform the validity checking, then the generated program would get stuck if there is an invalid predicate. So type checking is really a compile time approximation for the runtime behavior.  

Algorithmic typing is sound and complete w.r.t. declarative typing. 

\begin{definition}[Reduction]
  \fbox{$\Delta, \Sigma, \Phi \vdash t \to t'$}

  \
  
  \begin{tabular}{lll}
   \infer{\Delta, \Sigma, \Phi \vdash x \to t'}{x = t' \in \Delta}
   & &
   \infer{\Delta, [\Sigma, a_1 : [\underline{T}/\underline{X}]U_1 ], \Phi \vdash e \to f \ a_1}{(e: [\underline{T}/\underline{X}]U) \in \Sigma & (f : U_1 \Rightarrow U) \in \Phi}
   \\
   \\
   
   \infer{\Delta, \Sigma, \Phi \vdash (\lambda x.t)t' \to [t'/x]t}{}
   & &
  \infer{\Delta, \Sigma, \Phi \vdash t\ t_1 \to t'\ t_1}{\Delta, \Sigma, \Phi \vdash t \to t'}   
  \\
  \\
   
  \infer{\Delta, \Sigma, \Phi \vdash e \to f \ e_1}{(e: [\underline{T}/\underline{X}]U) \in \Sigma & (f : U_1 \Rightarrow U), (e_1 : [\underline{T}/\underline{X}]U_1 ) \in \Phi}
  \end{tabular}
  
  
\end{definition}

Note that we mentioned $\Phi$ is the logic program induced by instance declaration, we overload this symbol to denote the name annotation of the logic program. The let-expression in this article is treated as localised global definition, thus we do not need to define reduction directly on let-expression. 
\begin{definition}[Name Annotation]
  Let $\Phi = \{P_i \Rightarrow U_i\}_{i \in N}$, the name annotation of $\Phi$ is 
  $ \{e_i : \mathrm{curry}(P_i \to U_i)\}_{i \in N}$, where $e_i$ are term variable that are fresh and
  distinct. Note that $\mathrm{curry}$ stand for currying. 
\end{definition}

\begin{lemma}
  If $W(\Gamma, t) = ( t', S, \Sigma, \sigma)$, then $t'$ is progressive. 
\end{lemma}

\section{Preprocessing}
Preprocessing involves constructing dictionary for each type class and defining names introduced in name annotation.  

\begin{definition}
\

\begin{itemize}
  \item \textbf{Dictionary Construction}:   $\mathbf{class} \ U \ \mathbf{where}\ \{x_1 :  U \Rightarrow T_1,..., x_m :  U \Rightarrow T_m\ \}$ is used to generate $\mathbf{data} \ U \ \mathbf{where}\ \{ c_U : T_1 \to ... \to T_m \to U \}$ and $x_i = \lambda d . \mathbf{case}\ {d} \ \mathbf{of}\ \{c \ t_1 \ ...\ t_m \to t_i\}$. 
  \item \textbf{Name Definition}: $\mathbf{instance}\ U_1,..., U_n \Rightarrow U\ \mathbf{where}\ \{ x_1 = t_1, ..., x_m = t_m \}  $ is used to generate $e : U_1 \to ... \to U_n \to U = \lambda a_1 .... a_n . \mathbf{let}\ d = c_U (q_1 \ a_1...a_n\ d) ... (q_m \ a_1 ... a_n \ d)  \ \mathbf{in}\ d$, where $e$ is the name annotation of $U_1,..., U_n \Rightarrow U$, $q_i : U_1 \to ... \to U_n \to U \to T_i = \lambda a_1 ... a_n\ d . \hat{b}_i$, where $W(\Gamma, t_i) = (b_i, T_i, \Sigma_i, \sigma_i )$. Note that $\hat{b}_i$ is called \textit{renaming} by comparison of $a_1 : U_1,..., a_n : U_n, d: U$ and $\Sigma_i$, namely, for all $(e_j : U_j) \in \Sigma_i$, then all the $e_j$ in $b_i$ is renamed to $a_j$, if the type of $e_j$ is not any of $U_1,..., U_n, U$, then $e_j$ will be kept unchanged. 
  \end{itemize}

\end{definition}

Note that we are going to suport the notion of default implementation through overlapping instance declarations in this article, not through class declaration.  

Also, in Haskell, $\mathbf{class} \ U \ \mathbf{where}\ \{x_1 : T_1,..., x_m : T_m \}$ would means the same thing as $\mathbf{class} \ U \ \mathbf{where}\ \{x_1 :  U \Rightarrow T_1,..., x_m :  U \Rightarrow T_m\ \}$, we decided to go with latter in this article. 

\section{Example}

We will run the type checking algorithm and preprocessing manually to the following code. 
\begin{example}
  \
  
\begin{verbatim}
data Bool where
  true :: Bool
  false :: Bool
and = \ x y . case x of
               true -> y
               false -> false
data Nat where
  z :: Nat
  s :: Nat -> Nat
data List A where
  nil :: List A
  cons :: A -> List A -> List A
class Eq A where
  eq :: Eq A => A -> A -> Bool
instance Eq Nat where 
   eq = \ x y . case x of
                   z -> case y of
                           z -> true
                           s n -> false
                   s m -> case y of
                           z -> false
                           s n -> eq m n
instance Eq A => Eq (List A) where
   eq = \ l1 l2 . case l1 of 
                   nil -> case l2 of
                           nil -> true
                           cons y ys -> false
                   cons x xs -> case l2 of
                                 nil -> false
                                 cons y ys -> and (eq x y) (eq xs ys) 
test = eq (cons z nil) (cons z (cons z nil))
\end{verbatim}
\end{example}

\begin{procedure}[Type Checking Process]
  \

\begin{enumerate}
\item Collect typing context and perform dictionary construction:
  
  $\Gamma = \mathrm{true} : \mathsf{Bool}, \mathrm{false} : \mathsf{Bool}, z : \mathsf{Nat}, s : \mathsf{Nat} \to \mathsf{Nat},  \mathrm{nil} : \mathsf{List}\ A, \mathrm{cons} : A \to \mathsf{List}\ A \to \mathsf{List}\ A , \mathrm{eq} : \mathsf{Eq} \ A \Rightarrow A \to A \to \mathsf{Bool}, c : (A \to A \to \mathsf{Bool}) \to \mathsf{Eq} \ A$
  
  $\Delta = \mathrm{eq} = \lambda d . \mathbf{case}\ {d} \ \mathbf{of}\ \{c \ t \to t\}$
\item Name annotation:
  
  $\Phi = e_1 : \mathsf{Eq} \ \mathsf{Nat}, e_2 : \mathsf{Eq} \  A \to \mathsf{Eq} \ (\mathsf{List}\ A)$
 
  \item Type check instance declaration(name definition), but note that first we have to type check $\mathrm{and}$. So we add $\mathrm{and} : \mathsf{Bool} \to \mathsf{Bool} \to \mathsf{Bool}$ to the typing context. 
  \item Run name definition on $\mathsf{Eq} \ \mathsf{Nat}$:
    
    $\Delta = \Delta, e_1 = \mathbf{let}\ d = c (q_1  d) \ \mathbf{in}\ d$ where $q_1 = \lambda d. \hat{b}_1$, and $b_1$ is: 

\begin{verbatim}
  \ x y . case x of
                   z -> case y of
                           z -> true
                           s n -> false
                   s m -> case y of
                           z -> false
                           s n -> eq a1 m n
\end{verbatim}

\noindent $b_1$ is the generated term of type checking following code(abbreviated by $t_1$):

\begin{verbatim}
  \ x y . case x of
                   z -> case y of
                           z -> true
                           s n -> false
                   s m -> case y of
                           z -> false
                           s n -> eq m n
\end{verbatim}
  
\noindent We write $W(\Gamma, t_1) = (b_1, \mathsf{Nat} \to \mathsf{Nat} \to \mathsf{Bool}, [a_1 : \mathsf{Eq}\ \mathsf{Nat}],\_ )$. To rename $b_1$, we just change $a_1$ to $d$. So $\hat{b}_1$ is: 

\begin{verbatim}
  \ x y . case x of
                   z -> case y of
                           z -> true
                           s n -> false
                   s m -> case y of
                           z -> false
                           s n -> eq d m n
\end{verbatim}

\item Run name definition on $\mathsf{Eq} \ A \Rightarrow \mathsf{Eq} \ (\mathsf{List} \ A) $:
  
    $\Delta = \Delta, e_2 = \lambda a_1 . \mathbf{let}\ d = c\ (q_1\ a_1\ d) \ \mathbf{in}\ d$ where $ q_1 = \lambda  a_1 d. \hat{b}_1$, and $b_1$ is: 
  
\begin{verbatim}
\ l1 l2 . case l1 of 
                   nil -> case l2 of
                           nil -> true
                           cons y ys -> false
                   cons x xs -> case l2 of
                                 nil -> false
                                 cons y ys -> and (eq c1 x y) (eq c2 xs ys)   
\end{verbatim}

\noindent $b_1$ is the generated term of type checking following code(abbreviated by $t_1$):

\begin{verbatim}
\ l1 l2 . case l1 of 
                   nil -> case l2 of
                           nil -> true
                           cons y ys -> false
                   cons x xs -> case l2 of
                                 nil -> false
                                 cons y ys -> and (eq x y) (eq xs ys)   
\end{verbatim}


\noindent We write $W(\Gamma, t_1) = (b_1, \mathsf{List}\ A \to \mathsf{List}\ A \to \mathsf{Bool}, [c_1 : \mathsf{Eq}\ A, c_2 : \mathsf{Eq} (\mathsf{List}\ A)],\_ )$. To rename $b_1$, we just change $c_1$ to $a_1$, change $c_2$ to $d$. So $\hat{b}_1$ is: 

\begin{verbatim}
\ l1 l2 . case l1 of 
                   nil -> case l2 of
                           nil -> true
                           cons y ys -> false
                   cons x xs -> case l2 of
                                 nil -> false
                                 cons y ys -> and (eq a1 x y) (eq d xs ys)   
\end{verbatim}

\item Type check program $\mathrm{test}$, i.e. $W(\Gamma, \mathrm{test}) = (t', \mathsf{Bool}, [e_3 : \mathsf{Eq}(\mathsf{List}\ \mathsf{Nat})], \_)$, where $t'$ is:

\begin{verbatim}
  test = eq e3 (cons z nil) (cons z (cons z nil))
\end{verbatim}

\noindent We compare $e_3 : \mathsf{Eq}(\mathsf{List}\ \mathsf{Nat})$ and $\Phi$, notice that we don't need to rename $e_3$.
\item Reduction trace on $\mathrm{test}$ : 
  
  $\Delta, e_3 : \mathsf{Eq}(\mathsf{List}\ \mathsf{Nat}), \Phi \vdash \mathrm{test} \to \mathrm{eq}\ e_3\ (\mathrm{cons}\ z\ \mathrm{nil} ) (\mathrm{cons}\ z\ (\mathrm{cons}\ z\ \mathrm{nil})) \to (\mathbf{case}\ e_3\ \mathbf{of} \ \{c \ t \to t\})\ (\mathrm{cons}\ z\ \mathrm{nil} ) (\mathrm{cons}\ z\ (\mathrm{cons}\ z\ \mathrm{nil})) \to (\mathbf{case}\ (e_2\ e_1)\ \mathbf{of} \ \{c \ t \to t\})\ (\mathrm{cons}\ z\ \mathrm{nil} ) (\mathrm{cons}\ z\ (\mathrm{cons}\ z\ \mathrm{nil})) \to ...$
\end{enumerate}
\end{procedure}
\cite{Abadi:93}.
\bibliographystyle{plain}

% The bibliography should be embedded for final submission.
\bibliography{paper}

\end{document}
